ds:x:Id fp Type, da:k:Knd fp Type, A, B:ecl-trans-tuple{i:l}(ds;da),
f:((+Unit)()()), g:().
combine-ecl-tuples2(A;B;f;g)  ecl-trans-tuple{i:l}(ds;da) 

latex

Definitions

t  T, x:A. B(x), AB, P  Q, False, A, , State(ds), Valtype(da;k), Unit, , false, , x. t(x), 2of(t), 1of(t), p  q, reduce(f;k;as), Knd, (x  l), b, Prop, b, P & Q, P  Q, as @ bs, EqDecider(T), if b t else f fi, S  T, combine-halt-info(ea;eb;f;g;x), merge(as;bs), , let a,b,c,d,e,f,g = u in v(a;b;c;d;e;f;g), let x = a in b(x), combine-ecl-tuples2(A;B;f;g), ecl-trans-tuple{i:l}(ds;da), Id, a:A fp B(a), KindDeq, deq-member(eq;x;L)

Lemmas

ecl-trans-tuple wf, fpf wf, Id wf, it wf, merge wf, combine-halt-info wf, nat wf, ifthenelse wf, append wf, eqtt to assert, eqff to assert, iff transitivity, assert of bnot, not functionality wrt iff, assert-deq-member, deq-member wf, bnot wf, not wf, assert wf, l member wf, Knd wf, Kind-deq wf, reduce wf, bor wf, nat plus inc, pi1 wf, pi2 wf, nat plus wf, bfalse wf, bool wf, unit wf, ma-valtype wf, decl-state wf, le wf